/-- 
重复应用两个策略直到证明完成
参数：
- t₁: 第一个要应用的定理
- t₂: 第二个要应用的定理
-/
macro "repeat_apply" t₁:term "or" t₂:term : tactic => 
  `(tactic | repeat (first | apply $t₁ | apply $t₂))
  
macro "apply_until" t₁:term "until" t₂:term: tactic =>
  `(tactic | repeat (first | apply $t₁ | apply $t₂))